YES 0.459 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule Monad
  ((liftM3 :: (a  ->  d  ->  c  ->  b)  ->  Maybe a  ->  Maybe d  ->  Maybe c  ->  Maybe b) :: (a  ->  d  ->  c  ->  b)  ->  Maybe a  ->  Maybe d  ->  Maybe c  ->  Maybe b)

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM3 :: Monad e => (c  ->  b  ->  a  ->  d)  ->  e c  ->  e b  ->  e a  ->  e d
liftM3 f m1 m2 m3 = m1 >>= (\x1 ->m2 >>= (\x2 ->m3 >>= (\x3 ->return (f x1 x2 x3))))


module Maybe where
  import qualified Monad
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\x3→return (f x1 x2 x3)

is transformed to
liftM30 f x1 x2 x3 = return (f x1 x2 x3)

The following Lambda expression
\x2→m3 >>= liftM30 f x1 x2

is transformed to
liftM31 m3 f x1 x2 = m3 >>= liftM30 f x1 x2

The following Lambda expression
\x1→m2 >>= liftM31 m3 f x1

is transformed to
liftM32 m2 m3 f x1 = m2 >>= liftM31 m3 f x1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR

mainModule Monad
  ((liftM3 :: (a  ->  b  ->  c  ->  d)  ->  Maybe a  ->  Maybe b  ->  Maybe c  ->  Maybe d) :: (a  ->  b  ->  c  ->  d)  ->  Maybe a  ->  Maybe b  ->  Maybe c  ->  Maybe d)

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM3 :: Monad b => (a  ->  e  ->  c  ->  d)  ->  b a  ->  b e  ->  b c  ->  b d
liftM3 f m1 m2 m3 = m1 >>= liftM32 m2 m3 f

  
liftM30 f x1 x2 x3 = return (f x1 x2 x3)

  
liftM31 m3 f x1 x2 = m3 >>= liftM30 f x1 x2

  
liftM32 m2 m3 f x1 = m2 >>= liftM31 m3 f x1



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR

mainModule Monad
  ((liftM3 :: (c  ->  d  ->  a  ->  b)  ->  Maybe c  ->  Maybe d  ->  Maybe a  ->  Maybe b) :: (c  ->  d  ->  a  ->  b)  ->  Maybe c  ->  Maybe d  ->  Maybe a  ->  Maybe b)

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM3 :: Monad d => (a  ->  b  ->  c  ->  e)  ->  d a  ->  d b  ->  d c  ->  d e
liftM3 f m1 m2 m3 = m1 >>= liftM32 m2 m3 f

  
liftM30 f x1 x2 x3 = return (f x1 x2 x3)

  
liftM31 m3 f x1 x2 = m3 >>= liftM30 f x1 x2

  
liftM32 m2 m3 f x1 = m2 >>= liftM31 m3 f x1


module Maybe where
  import qualified Monad
import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow

mainModule Monad
  (liftM3 :: (a  ->  d  ->  c  ->  b)  ->  Maybe a  ->  Maybe d  ->  Maybe c  ->  Maybe b)

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  liftM3 :: Monad b => (c  ->  a  ->  d  ->  e)  ->  b c  ->  b a  ->  b d  ->  b e
liftM3 f m1 m2 m3 = m1 >>= liftM32 m2 m3 f

  
liftM30 f x1 x2 x3 = return (f x1 x2 x3)

  
liftM31 m3 f x1 x2 = m3 >>= liftM30 f x1 x2

  
liftM32 m2 m3 f x1 = m2 >>= liftM31 m3 f x1



Haskell To QDPs